l1,l2:IdLnk, tg1,tg2:Id.
(rcv(l1,tg1) = rcv(l2,tg2)  Knd)  guard(((l1 = l2)  (tg1 = tg2))) 

latex

Definitions	x:A. B(x), P  Q, t  T, prop{i:l}, guard(T), x. t(x), Knd, rcv(l,tg), x(s)
Lemmas	Knd wf, rcv wf, Id wf, IdLnk wf, pi1 wf, pi2 wf